IUnivData.agda:3,6-13
The sort of BadData cannot be the interval universe IUniv
when checking the definition of BadData
